Nuprl Definition : p-open 11,40

p-open(p)
== {C:(n:  ({0..n}Outcome)){0..2}| 
== {s:(Outcome), j:, i:{0..j}. (C(<i, s>))  (C(<j, s>))}  
latex



clarification:

p-open(p)
== {C:(n:  ({0..n}p-outcome(p))){0..2}| 
== {s:(p-outcome(p)), j:, i:{0..j}. (C(<i, s>))  (C(<j, s>))}  
latex


Definitions{x:A| B(x)} , x:A  B(x), x:AB(x), Outcome, , x:A. B(x), {i..j}, #$n, A  B, f(a), <a, b>
FDL editor aliasesp-open

origin